Nuprl Lemma : es-choose_wf
0,22
postcript
pdf
es
:ES,
i
:Id. Choose(
i
)
b
:Id
(
x
:Id
vartype(
i
;
x
))
(kindtype(
i
;locl(
b
))+Unit)
latex
Definitions
Unit
,
Type
,
t
T
,
f
(
a
)
,
left
+
right
,
Id
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
act(
k
)
,
locl(
a
)
,
tag(
k
)
,
lnk(
k
)
,
isrcv(
k
)
,
if
b
t
else
f
fi
,
P
&
Q
,
es-Choose(
es
)
,
es-V(
es
)
,
es-M(
es
)
,
es-T(
es
)
,
Choose(
i
)
,
kindtype(
i
;
k
)
,
vartype(
i
;
x
)
,
x
:
A
B
(
x
)
,
ES
Lemmas
event
system
wf
,
Id
wf
,
unit
wf
origin
es:ES, i:Id. Choose(i) 
b:Id
(x:Idvartype(i;x))(kindtype(i;locl(b))+Unit) es:ES, i:Id. Choose(i) b:Id(x:Idvartype(i;x))(kindtype(i;locl(b))+Unit) TB(x)x:A. B(x)
t else f fi
B(x)